FDL - Nuprl Lemma : K-refine

Nuprl Lemma : K-refine

Pgm, Sem:Type, equiv:(Sem

Sem

), X:(Sem

), S:(Pgm

Sem), pr:Pgm, kpr:(Sem

Pgm).
pr implements kpr

kpr |= X

pr |= X

Definitions t T, pr |= X, P Q, , x:A. B(x), kpr |= X, pr implements kpr

Lemmas K-implements wf, K-sem-sat wf